Stale. Unit tests for this workload were added in commit ecb3983 under jepsen/test/elastickv/redis_zset_safety_workload_test.clj — they cover test-spec construction (builds-test-spec, custom-options-override-defaults) plus checker edge cases: no-op ZREM, :info ZINCRBY, phantoms, stale reads, superseded scores, concurrent ZADD/ZREM, :info ZREM absence, :info ZINCRBY completeness, infinity parsing, duplicate-member flagging. Latest commit 0c0efc4 adds two more for the single-ok / multi-ZINCRBY score check.

Stale. ZREM now carries :removed? from the server reply into the mutation record (see completed-mutation-window lines 283-295 and apply-mutation-to-state/existence-evidence?). A no-op ZREM (returns 0) does NOT mutate model state, and :info/:pending ZREMs are treated as possibly-concurrent deletions via the concurrent window. Regression test: noop-zrem-does-not-flag-correct-read and no-op-zrem-alone-does-not-false-positive. Landed in 2a194a4 / ecb3983.

Stale. completed-mutation-window sets :unknown-score? on each :info/:pending ZINCRBY (line 277-279), and allowed-scores-for-member propagates that to the caller so check-zrange-all/check-zrangebyscore skip strict score validation when the resulting score is unknown. Regression test: info-zincrby-skips-strict-score-check, info-before-read-is-considered-uncertain. Landed in 2a194a4 / ecb3983, refined in 0c0efc4 per Codex P1.

Stale. Docstring rewritten on line 323-327: "Construct authoritative per-member state from mutations whose completions strictly precede read-inv-idx. Returns {member -> {:present? bool :score s}}". The {:members map :ok-members set} wording no longer appears in the file.

Stale. jepsen_test.clj now dispatches on the first positional arg via the test-fns map (lines 21-29), auto-prepending test if the user omitted the jepsen subcommand. elastickv-zset-safety-test is reachable via lein run -m elastickv.jepsen-test elastickv-zset-safety-test .... The workload namespace's own -main also works for direct invocation.

The use of Double/parseDouble directly on Redis score strings will fail if the score is infinite. Redis returns "inf", "+inf", or "-inf" for infinite values, but Java's Double/parseDouble expects "Infinity" or "-Infinity". This will cause a NumberFormatException during the test if infinite scores are encountered.

(defn- parse-double-safe
  "Parses a Redis score string into a Double, handling 'inf' representations."
  [s]
  (let [s-str (str/lower-case (str s))]
    (cond
      (str/includes? s-str "inf") (if (str/starts-with? s-str "-")
                                     Double/NEGATIVE_INFINITY
                                     Double/POSITIVE_INFINITY)
      :else (Double/parseDouble (str s)))))

(defn- parse-withscores
  "Carmine returns a flat [member score member score ...] vector for
  ZRANGE WITHSCORES. Convert to a sorted vector of [member (double score)]
  preserving server-returned order (score ascending, then member)."
  [flat]
  (->> flat
       (partition 2)
       (mapv (fn [[m s]]
               [(if (bytes? m) (String. ^bytes m) (str m))
                (parse-double-safe s)]))))

Stale. parse-double-safe (lines 71-87) normalizes inf / +inf / -inf (and JVM-style Infinity) before falling through to Double/parseDouble. parse-withscores calls it on every returned score. Regression test: parse-withscores-handles-inf-strings. Landed in ecb3983.

As noted in the parse-withscores feedback, Double/parseDouble should be replaced with a safe parser that handles Redis's "inf" strings.

                   :value [member (parse-double-safe new-score)]]))

Stale. The :zincrby branch of invoke! already calls parse-double-safe on the server-returned score (line 134). Covered by parse-withscores-handles-inf-strings plus the infinity branch in parse-double-safe. Landed in ecb3983.

The current implementation of allowed-scores-for-member is too permissive and potentially unsound for linearizability checks.

1. Stale Reads: It includes all successful committed scores in the scores set (line 384), even if they were strictly followed by a later committed mutation. In a linearizable system, a read should only observe scores from the "potentially latest" committed writes (those not strictly followed by another) or concurrent ones.
2. Stale Presence: The checker does not verify if a member is allowed to be present. If a member was added and then deleted (both committed before the read), any-known? remains true, and the read will accept the member even though it should be absent.
3. Efficiency: The committed-overlap? check (line 368) is $O(N^2)$ relative to the number of mutations for a member. While the member universe is small, this can be optimized to $O(N)$ by tracking the maximum invoke-idx of preceding mutations.

(defn- allowed-scores-for-member
  "Compute the set of scores considered valid for `member` by a read
  whose window is [read-inv-idx, read-cmp-idx], based on committed state
  and any concurrent mutations."
  [mutations-by-m member read-inv-idx read-cmp-idx]
  (let [muts (get mutations-by-m member [])
        ;; Mutations that completed strictly before the read started.
        preceding (filter #(and (= :ok (:type %))
                                (some? (:complete-idx %))
                                (< (:complete-idx %) read-inv-idx))
                          muts)
        ;; A mutation is a candidate for the 'latest' state if no other
        ;; committed mutation strictly follows it (m2.invoke > m.complete).
        max-inv (reduce max -1 (map :invoke-idx preceding))
        candidates (filter #(>= (:complete-idx %) max-inv) preceding)

        concurrent (concurrent-mutations-for-member muts read-inv-idx read-cmp-idx)
        pre-read-info (filter #(and (= :info (:type %))
                                    (some? (:complete-idx %))
                                    (< (:complete-idx %) read-inv-idx))
                              muts)

        ;; Scores allowed by committed state or uncertain ops.
        scores (into (set (keep :score candidates))
                     (concat (keep :score concurrent)
                             (keep :score pre-read-info)))

        unknown-score? (some #(and (= :zincrby (:f %)) (:unknown-score? %))
                             (concat concurrent pre-read-info))

        ;; Allowed to be present if any candidate or concurrent/info op is a write.
        can-be-present? (or (some #(#{:zadd :zincrby} (:f %)) candidates)
                            (some #(#{:zadd :zincrby} (:f %)) concurrent)
                            (some #(#{:zadd :zincrby} (:f %)) pre-read-info))

        ;; Must be present if all candidates are writes and no concurrent/info op can delete.
        must-be-present? (and (seq candidates)
                              (every? #(#{:zadd :zincrby} (:f %)) candidates)
                              (not (some #(= :zrem (:f %)) concurrent))
                              (not (some #(= :zrem (:f %)) pre-read-info)))]
    {:scores scores
     :unknown-score? (boolean unknown-score?)
     :must-be-present? must-be-present?
     :can-be-present? can-be-present?}))

Stale. allowed-scores-for-member now applies a real-time last-wins max-inv filter to committed mutations (lines 408-411): a preceding mutation is admissible only when no other preceding mutation's invoke strictly follows it. Superseded scores are excluded from :scores. Presence-under-stale-reads is caught by can-be-present? (lines 466-469), which is checked in both check-zrange-all (line 529) and check-zrangebyscore (line 590). Regression tests: superseded-committed-score-is-not-allowed, stale-read-after-committed-zrem-is-flagged, phantom-member-is-flagged. Landed in 2a194a4.

The phantom check should be replaced with a more robust can-be-present? check to catch both phantoms (never existed) and stale reads (present after a committed deletion).

    (doseq [[member score] entries]
      (let [{:keys [scores can-be-present? unknown-score?]}
            (allowed-scores-for-member mutations-by-m member inv-idx cmp-idx)]
        (cond
          (not can-be-present?)
          (swap! errors conj {:kind :unexpected-presence
                              :index cmp-idx
                              :member member
                              :score score})

Stale. check-zrange-all (line 529) and check-zrangebyscore (line 590) both use (not can-be-present?) to emit :unexpected-presence / :unexpected-presence-range. can-be-present? (returned from allowed-scores-for-member) covers both phantoms (no existence evidence anywhere) and stale reads (committed-removed before the read). Regression tests: phantom-member-is-flagged, stale-read-after-committed-zrem-is-flagged. Landed in 2a194a4.

The logic in allowed-scores-for-member has several correctness issues that will lead to false positives and false negatives in safety checking:

1. False Positives (Strictness): candidate-present? relies on complete-idx order to determine presence. In a linearizable system, concurrent committed operations can be serialized in any order. If a ZADD and ZREM are concurrent but both finish before the read, the read may legitimately observe either state. The current logic flags one of these as an error.
2. False Negatives (Completeness): must-be-present? is too strict. It returns false if any uncertain operation exists, even if that operation is a ZADD which cannot remove the member. It should only be false if an uncertain or concurrent removal exists.
3. ZINCRBY Score Set: For multiple concurrent ZINCRBY operations, the set of allowed scores should include all possible prefix sums of the increments. The current logic only includes the final score of each increment, which is too restrictive.

The suggested fix relaxes can-be-present? to allow any valid serialization of candidates and uncertain operations, and refines must-be-present? to correctly identify when a member is required to appear.

  (let [muts (get mutations-by-m member [])
        ;; :ok mutations that completed strictly before the read.
        preceding (->> muts
                       (filter #(and (= :ok (:type %))
                                     (some? (:complete-idx %))
                                     (< (:complete-idx %) read-inv-idx))))
        ;; Real-time "last-wins" candidate filter: a preceding mutation
        ;; m is admissible iff no OTHER preceding mutation m' has
        ;; m'.invoke-idx > m.complete-idx (i.e. m' strictly follows m).
        max-inv (reduce max -1 (map :invoke-idx preceding))
        candidates (filterv #(>= (:complete-idx %) max-inv) preceding)
        ;; :info mutations that completed before the read: they may or
        ;; may not have taken effect server-side.
        pre-read-info (->> muts
                           (filter #(and (= :info (:type %))
                                         (some? (:complete-idx %))
                                         (< (:complete-idx %) read-inv-idx))))
        ;; Concurrent mutations: windows overlap the read. Include both
        ;; :ok and :info since either may have taken effect.
        concurrent (concurrent-mutations-for-member muts read-inv-idx read-cmp-idx)
        all-uncertain (concat pre-read-info concurrent)

        add-scores (fn [acc m]
                     (case (:f m)
                       :zadd    (conj acc (:score m))
                       :zincrby (cond-> acc (some? (:score m)) (conj (:score m)))
                       :zrem    acc))
        ;; Admissible scores: candidate committed + pre-read :info +
        ;; concurrent writes (with a known score).
        scores (as-> #{} s
                 (reduce add-scores s candidates)
                 (reduce add-scores s all-uncertain))

        ;; Relax score check if any ZINCRBY is concurrent or uncertain.
        ;; Multiple concurrent increments can produce intermediate sums not in `scores`.
        unknown-score? (some #(= :zincrby (:f %)) all-uncertain)

        ;; can-be-present?: true if any candidate or uncertain op results in presence.
        can-be-present? (or (some write-op? candidates)
                            (some write-op? all-uncertain)
                            (some existence-evidence? (concat candidates all-uncertain)))

        ;; must-be-present?: true if ALL valid serializations result in presence.
        must-be-present? (and (some write-op? candidates)
                              (not (some #(= :zrem (:f %)) candidates))
                              (not (some #(= :zrem (:f %)) all-uncertain)))]
    {:scores           scores
     :unknown-score?   (boolean unknown-score?)
     :can-be-present?  (boolean can-be-present?)
     :must-be-present? must-be-present?})

Partially stale, partially rebutted.

False Positives (Strictness) — addressed in 2a194a4. Overlapping-window committed ops are both admissible: max-inv = max of preceding :invoke-idx; candidates = preceding ops with :complete-idx >= max-inv. When multiple candidates remain their windows overlap, so any can serialize last, and candidate-can-be-present? / candidate-can-be-absent? both consider them. Regression tests: concurrent-zadd-zrem-both-completed-accepts-either-outcome (both [["m1" 1.0]] and [] accepted), overlapping-committed-zadds-allow-either-score.

False Negatives (Completeness on must-be-present?) — I don't see this in the code. must-be-present? (lines 475-477) guards on any-candidate-write?, (not candidate-can-be-absent?), and (not any-uncertain-zrem?). Uncertain ZADDs do NOT force it to false; only uncertain ZREMs do, which is correct (a ZREM could reorder last and remove the member). Could you point to the exact path that triggers the false negative?

The completeness check for ZRANGE is currently too simple and doesn't account for :info operations that might have removed a member before the read. It should use the must-be-present? logic from allowed-scores-for-member which correctly handles uncertain removals.

    (let [model (model-before mutations-by-m inv-idx)
          observed-members (into #{} (map first) entries)]
      (doseq [[member _] model]
        (let [{:keys [must-be-present?]} (allowed-scores-for-member mutations-by-m member inv-idx cmp-idx)]
          (when (and must-be-present? (not (contains? observed-members member)))
            (swap! errors conj {:kind :missing-member
                                :index cmp-idx
                                :member member}))))
      @errors))

Stale. check-zrange-all completeness (lines 549-558) already uses must-be-present? from allowed-scores-for-member, which correctly skips members that an :info or concurrent ZREM might have removed. Regression test: info-zrem-concurrent-with-read-allows-missing-member. Landed in 2a194a4.

The completeness check for ZRANGEBYSCORE has the same issue as ZRANGE: it doesn't account for uncertain removals. Additionally, it should only enforce completeness if the score is definitively known to be within the requested range (i.e., no uncertain increments).

    ;; Completeness within bounds: any model member whose committed score
    ;; is in [lo,hi] with no concurrent mutation must appear.
    (let [model (model-before mutations-by-m inv-idx)
          observed-members (into #{} (map first) members)]
      (doseq [[member _] model]
        (let [{:keys [must-be-present? scores unknown-score?]} (allowed-scores-for-member mutations-by-m member inv-idx cmp-idx)]
          (when (and must-be-present?
                     (not unknown-score?)
                     (every? #(<= lo % hi) scores)
                     (not (contains? observed-members member)))
            (swap! errors conj {:kind :missing-member-range
                                :index cmp-idx
                                :bounds bounds
                                :member member
                                :expected-score (first scores)}))))
      @errors))

Stale. check-zrangebyscore completeness (lines 610-623) uses both must-be-present? AND score-definitely-in-range? (which requires (not unknown-score?) and every candidate score inside [lo, hi]). Uncertain ZINCRBYs → unknown-score? → no completeness failure. Regression test: info-zincrby-does-not-flag-zrangebyscore-completeness. Landed in 2a194a4.

Keep score validation enabled for known concurrent ZINCRBY

allowed-scores-for-member marks :unknown-score? true whenever any uncertain mutation is :zincrby, even when that op completed :ok with a known resulting score. Both check-zrange-all and check-zrangebyscore then skip score-membership validation when :unknown-score? is true, so a read concurrent with a known ZINCRBY can return an impossible score (e.g., 999.0) without being flagged. This creates false negatives in the new safety checker and weakens the core score-correctness guarantee under concurrency.

Useful? React with 👍 / 👎.

Addressed in 0c0efc4. unknown-score? is now set only when an individual ZINCRBY's own score is unknown (:info/:pending — the :unknown-score? flag set in completed-mutation-window), or when there are >=2 concurrent/uncertain ZINCRBYs where prefix-sum intermediates can occur. A single :ok concurrent ZINCRBY no longer waves through impossible scores. Regression test: single-ok-concurrent-zincrby-still-validates-scores (read returning 999.0 alongside one :ok ZINCRBY is flagged :score-mismatch).

Reject vacuous pass when no successful reads exist

The checker currently reports success whenever all-errors is empty, but all-errors is built only from :ok read completions. If Redis is unreachable or misconfigured (e.g., bad host/port), invoke! downgrades ops to :info, read-pairs becomes empty, and this returns :valid? true even though no safety property was actually exercised. That can produce false-green CI runs for a broken test environment; the checker should mark this case invalid/unknown (or enforce a minimum successful-read count).

Useful? React with 👍 / 👎.

While logging a warning is helpful, failing to clear the zset-key during setup! can lead to false-positive safety results if stale data from a previous run survives. Given that this is a safety-focused workload, it is generally safer to throw an exception and abort the run if the initial state cannot be guaranteed clean, rather than proceeding with a warning.

If car/wcar returns nil (which can happen in some Carmine configurations during protocol edge cases or timeouts if not configured to throw), the call to (long removed) will throw a NullPointerException. Although this is caught by the general Exception handler at line 225 and converted to an :info op, it's better to handle the potential nil explicitly to avoid unnecessary stack traces in logs.

            (assoc op :type :ok :value [member (pos? (long (or removed 0)))])

Setting :final-generator to nil disables the quiescent check at the end of the Jepsen run. While the comment notes a serialization issue in Jepsen 0.3.x, this means the workload loses the ability to verify that the system eventually reaches a consistent state after faults stop. If the serialization issue is specific to complex generators, consider using a simpler, non-combined generator for the final check instead of disabling it entirely.